YES 11.118
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule Main
| ((readDec :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Lambda Reductions:
The following Lambda expression
\nd→n * radix + d
is transformed to
readInt0 | radix n d | = n * radix + d |
The following Lambda expression
\vu77→
case | vu77 of |
| (ds,r) | → (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
| _ | → [] |
is transformed to
readInt1 | radix digToInt vu77 | =
case | vu77 of | | (ds,r) | → (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
| _ | → [] |
|
The following Lambda expression
\d→fromEnum d - fromEnum_0
is transformed to
readDec0 | d | = fromEnum d - fromEnum_0 |
The following Lambda expression
\vu68→
case | vu68 of |
| (cs@(_ : _),t) | → (cs,t) : [] |
| _ | → [] |
is transformed to
nonnull0 | vu68 | =
case | vu68 of | | (cs@(_ : _),t) | → (cs,t) : [] |
| _ | → [] |
|
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule Main
| ((readDec :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Case Reductions:
The following Case expression
case | vu77 of |
| (ds,r) | → (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
| _ | → [] |
is transformed to
readInt10 | radix digToInt (ds,r) | = (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
readInt10 | radix digToInt _ | = [] |
The following Case expression
case | vu68 of |
| (cs@(_ : _),t) | → (cs,t) : [] |
| _ | → [] |
is transformed to
nonnull00 | (cs@(_ : _),t) | = (cs,t) : [] |
nonnull00 | _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
mainModule Main
| ((readDec :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
cs@(vy : vz)
is replaced by the following term
vy : vz
The bind variable of the following binding Pattern
xs@(ww : wx)
is replaced by the following term
ww : wx
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((readDec :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
span | p [] | = ([],[]) |
span | p (ww : wx) | |
is transformed to
span | p [] | = span3 p [] |
span | p (ww : wx) | = span2 p (ww : wx) |
span2 | p (ww : wx) | =
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
|
span3 | p [] | = ([],[]) |
span3 | xx xy | = span2 xx xy |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule Main
| ((readDec :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Let/Where Reductions:
The bindings of the following Let/Where expression
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
are unpacked to the following functions on top level
span2Ys | xz yu | = span2Ys0 xz yu (span2Vu43 xz yu) |
span2Vu43 | xz yu | = span xz yu |
span2Zs | xz yu | = span2Zs0 xz yu (span2Vu43 xz yu) |
span2Span0 | xz yu p ww wx True | = ([],ww : wx) |
span2Span1 | xz yu p ww wx True | = (ww : span2Ys xz yu,span2Zs xz yu) |
span2Span1 | xz yu p ww wx False | = span2Span0 xz yu p ww wx otherwise |
span2Zs0 | xz yu (wz,zs) | = zs |
span2Ys0 | xz yu (ys,wy) | = ys |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
mainModule Main
| ((readDec :: [Char] -> [(Int,[Char])]) :: [Char] -> [(Int,[Char])]) |
module Main where
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule Main
| (readDec :: [Char] -> [(Int,[Char])]) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs0(Char(Succ(yv7000)), yv71, yv72, yv73) → new_span2Zs00(yv7000, yv71, yv7000, yv72, yv73)
new_span2Zs00(yv92, yv93, Succ(yv940), Zero, yv96) → new_span2Zs01(yv92, yv93, Succ(yv92), Succ(yv96))
new_span2Zs01(yv113, yv114, Zero, Zero) → new_span2Zs03(yv113, yv114)
new_span2Zs(:(yv600, yv601)) → new_span2Zs0(yv600, yv601, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs02(yv92, yv93, yv96) → new_span2Zs01(yv92, yv93, Succ(yv92), Succ(yv96))
new_span2Zs01(yv113, yv114, Succ(yv1150), Succ(yv1160)) → new_span2Zs01(yv113, yv114, yv1150, yv1160)
new_span2Zs00(yv92, yv93, Zero, Zero, yv96) → new_span2Zs02(yv92, yv93, yv96)
new_span2Zs01(yv113, yv114, Zero, Succ(yv1160)) → new_span2Zs(yv114)
new_span2Zs00(yv92, yv93, Succ(yv940), Succ(yv950), yv96) → new_span2Zs00(yv92, yv93, yv940, yv950, yv96)
new_span2Zs03(yv113, yv114) → new_span2Zs(yv114)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs01(yv113, yv114, Succ(yv1150), Succ(yv1160)) → new_span2Zs01(yv113, yv114, yv1150, yv1160)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
- new_span2Zs00(yv92, yv93, Succ(yv940), Succ(yv950), yv96) → new_span2Zs00(yv92, yv93, yv940, yv950, yv96)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5
- new_span2Zs0(Char(Succ(yv7000)), yv71, yv72, yv73) → new_span2Zs00(yv7000, yv71, yv7000, yv72, yv73)
The graph contains the following edges 1 > 1, 2 >= 2, 1 > 3, 3 >= 4, 4 >= 5
- new_span2Zs(:(yv600, yv601)) → new_span2Zs0(yv600, yv601, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
The graph contains the following edges 1 > 1, 1 > 2
- new_span2Zs03(yv113, yv114) → new_span2Zs(yv114)
The graph contains the following edges 2 >= 1
- new_span2Zs01(yv113, yv114, Zero, Succ(yv1160)) → new_span2Zs(yv114)
The graph contains the following edges 2 >= 1
- new_span2Zs00(yv92, yv93, Succ(yv940), Zero, yv96) → new_span2Zs01(yv92, yv93, Succ(yv92), Succ(yv96))
The graph contains the following edges 1 >= 1, 2 >= 2
- new_span2Zs00(yv92, yv93, Zero, Zero, yv96) → new_span2Zs02(yv92, yv93, yv96)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 >= 3
- new_span2Zs01(yv113, yv114, Zero, Zero) → new_span2Zs03(yv113, yv114)
The graph contains the following edges 1 >= 1, 2 >= 2
- new_span2Zs02(yv92, yv93, yv96) → new_span2Zs01(yv92, yv93, Succ(yv92), Succ(yv96))
The graph contains the following edges 1 >= 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMinusNat(Succ(yv890), Succ(yv900)) → new_primMinusNat(yv890, yv900)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMinusNat(Succ(yv890), Succ(yv900)) → new_primMinusNat(yv890, yv900)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(yv1980), Succ(yv18200)) → new_primPlusNat(yv1980, yv18200)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(yv1980), Succ(yv18200)) → new_primPlusNat(yv1980, yv18200)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(yv17600), yv175) → new_primMulNat(yv17600, yv175)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(yv17600), yv175) → new_primMulNat(yv17600, yv175)
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldl(yv145, yv146, yv147, yv148, Succ(yv1490), Zero, yv151, ba) → new_foldl0(yv145, yv146, yv147, yv148, Succ(yv147), Succ(yv151), ba)
new_foldl2(yv175, yv176, yv177, yv178, yv181, bb) → new_foldl4(yv175, yv176, new_pt(yv177, bb), yv178, bb)
new_foldl(yv145, yv146, yv147, yv148, Succ(yv1490), Succ(yv1500), yv151, ba) → new_foldl(yv145, yv146, yv147, yv148, yv1490, yv1500, yv151, ba)
new_foldl(yv145, yv146, yv147, yv148, Zero, Zero, yv151, ba) → new_foldl1(yv145, yv146, yv147, yv148, yv151, ba)
new_foldl6(yv132, yv139, Char(Succ(yv13500)), yv136, yv137, yv138, bd) → new_foldl(yv132, yv139, yv13500, yv136, yv13500, yv137, yv138, bd)
new_foldl1(yv145, yv146, yv147, yv148, yv151, ba) → new_foldl0(yv145, yv146, yv147, yv148, Succ(yv147), Succ(yv151), ba)
new_foldl3(yv175, yv176, yv177, yv178, bb) → new_foldl2(yv175, yv176, yv177, yv178, new_span2Zs1(yv178), bb)
new_foldl5(yv191, yv192, yv193, yv194, yv195, yv196, yv197, bc) → new_foldl6(yv191, new_readInt0(yv191, yv192, yv193, bc), yv194, yv195, yv196, yv197, bc)
new_foldl0(yv175, yv176, yv177, yv178, Zero, Succ(yv1800), bb) → new_foldl2(yv175, yv176, yv177, yv178, new_span2Zs1(yv178), bb)
new_foldl0(yv175, yv176, yv177, yv178, Succ(yv1790), Succ(yv1800), bb) → new_foldl0(yv175, yv176, yv177, yv178, yv1790, yv1800, bb)
new_foldl0(yv175, yv176, yv177, yv178, Zero, Zero, bb) → new_foldl3(yv175, yv176, yv177, yv178, bb)
new_foldl4(yv175, yv176, yv182, :(yv1780, yv1781), bb) → new_foldl5(yv175, yv176, yv182, yv1780, yv1781, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))), bb)
The TRS R consists of the following rules:
new_span2Zs05(yv92, yv93, Succ(yv940), Zero, yv96) → new_span2Zs08(yv92, yv93, yv96)
new_readInt0(yv175, Neg(yv1760), Neg(yv1820), ty_Int) → Neg(new_primPlusNat0(new_primMulNat0(yv1760, yv175), yv1820))
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_pt(yv61, ty_Int) → new_primMinusInt(yv61, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))
new_primMulNat0(Succ(yv17600), yv175) → new_primPlusNat0(new_primMulNat0(yv17600, yv175), Succ(yv175))
new_primMulNat0(Zero, yv175) → Zero
new_primMinusNat0(Zero, Succ(yv900)) → Neg(Succ(yv900))
new_primPlusNat0(Succ(yv1980), Succ(yv18200)) → Succ(Succ(new_primPlusNat0(yv1980, yv18200)))
new_primMinusInt(yv89, yv90) → new_primMinusNat0(yv89, yv90)
new_span2Zs05(yv92, yv93, Zero, Zero, yv96) → new_span2Zs08(yv92, yv93, yv96)
new_span2Zs05(yv92, yv93, Succ(yv940), Succ(yv950), yv96) → new_span2Zs05(yv92, yv93, yv940, yv950, yv96)
new_span2Zs010(yv113, yv114) → new_span2Zs06(yv113, yv114, new_span2Zs1(yv114))
new_span2Zs04(Char(Zero), yv71, yv72, yv73) → :(Char(Zero), yv71)
new_readInt0(yv175, Pos(yv1760), Neg(yv1820), ty_Int) → new_primMinusNat0(new_primMulNat0(yv1760, yv175), yv1820)
new_readInt0(yv175, Neg(yv1760), Pos(yv1820), ty_Int) → new_primMinusNat0(yv1820, new_primMulNat0(yv1760, yv175))
new_span2Zs09(yv113, yv114, Succ(yv1150), Succ(yv1160)) → new_span2Zs09(yv113, yv114, yv1150, yv1160)
new_span2Zs07(yv92, yv93) → :(Char(Succ(yv92)), yv93)
new_primPlusNat0(Zero, Zero) → Zero
new_span2Zs09(yv113, yv114, Succ(yv1150), Zero) → new_span2Zs07(yv113, yv114)
new_span2Zs08(yv92, yv93, yv96) → new_span2Zs09(yv92, yv93, Succ(yv92), Succ(yv96))
new_span2Zs1([]) → []
new_span2Zs1(:(yv600, yv601)) → new_span2Zs04(yv600, yv601, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs05(yv92, yv93, Zero, Succ(yv950), yv96) → new_span2Zs07(yv92, yv93)
new_span2Zs09(yv113, yv114, Zero, Succ(yv1160)) → new_span2Zs010(yv113, yv114)
new_readInt0(yv175, Pos(yv1760), Pos(yv1820), ty_Int) → Pos(new_primPlusNat0(new_primMulNat0(yv1760, yv175), yv1820))
new_pt(yv61, ty_Integer) → error([])
new_readInt0(yv175, yv176, yv182, ty_Integer) → error([])
new_primMinusNat0(Succ(yv890), Zero) → Pos(Succ(yv890))
new_span2Zs09(yv113, yv114, Zero, Zero) → new_span2Zs010(yv113, yv114)
new_primPlusNat0(Zero, Succ(yv18200)) → Succ(yv18200)
new_primPlusNat0(Succ(yv1980), Zero) → Succ(yv1980)
new_span2Zs04(Char(Succ(yv7000)), yv71, yv72, yv73) → new_span2Zs05(yv7000, yv71, yv7000, yv72, yv73)
new_primMinusNat0(Succ(yv890), Succ(yv900)) → new_primMinusNat0(yv890, yv900)
new_span2Zs06(yv113, yv114, yv118) → yv118
The set Q consists of the following terms:
new_span2Zs08(x0, x1, x2)
new_span2Zs09(x0, x1, Zero, Succ(x2))
new_span2Zs04(Char(Succ(x0)), x1, x2, x3)
new_primMinusInt(x0, x1)
new_readInt0(x0, Neg(x1), Neg(x2), ty_Int)
new_span2Zs05(x0, x1, Succ(x2), Zero, x3)
new_span2Zs05(x0, x1, Zero, Succ(x2), x3)
new_primMinusNat0(Succ(x0), Zero)
new_span2Zs06(x0, x1, x2)
new_span2Zs09(x0, x1, Zero, Zero)
new_span2Zs1(:(x0, x1))
new_span2Zs04(Char(Zero), x0, x1, x2)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_span2Zs010(x0, x1)
new_primMinusNat0(Zero, Zero)
new_readInt0(x0, Pos(x1), Pos(x2), ty_Int)
new_primPlusNat0(Zero, Succ(x0))
new_primMinusNat0(Zero, Succ(x0))
new_span2Zs1([])
new_readInt0(x0, x1, x2, ty_Integer)
new_readInt0(x0, Neg(x1), Pos(x2), ty_Int)
new_readInt0(x0, Pos(x1), Neg(x2), ty_Int)
new_primMinusNat0(Succ(x0), Succ(x1))
new_pt(x0, ty_Int)
new_span2Zs05(x0, x1, Succ(x2), Succ(x3), x4)
new_pt(x0, ty_Integer)
new_primPlusNat0(Zero, Zero)
new_span2Zs09(x0, x1, Succ(x2), Zero)
new_primMulNat0(Zero, x0)
new_span2Zs07(x0, x1)
new_span2Zs05(x0, x1, Zero, Zero, x2)
new_span2Zs09(x0, x1, Succ(x2), Succ(x3))
new_primMulNat0(Succ(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldl4(yv175, yv176, yv182, :(yv1780, yv1781), bb) → new_foldl5(yv175, yv176, yv182, yv1780, yv1781, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))), bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 4 > 5, 5 >= 8
- new_foldl0(yv175, yv176, yv177, yv178, Succ(yv1790), Succ(yv1800), bb) → new_foldl0(yv175, yv176, yv177, yv178, yv1790, yv1800, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 > 5, 6 > 6, 7 >= 7
- new_foldl(yv145, yv146, yv147, yv148, Succ(yv1490), Succ(yv1500), yv151, ba) → new_foldl(yv145, yv146, yv147, yv148, yv1490, yv1500, yv151, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 > 5, 6 > 6, 7 >= 7, 8 >= 8
- new_foldl6(yv132, yv139, Char(Succ(yv13500)), yv136, yv137, yv138, bd) → new_foldl(yv132, yv139, yv13500, yv136, yv13500, yv137, yv138, bd)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 3 > 5, 5 >= 6, 6 >= 7, 7 >= 8
- new_foldl5(yv191, yv192, yv193, yv194, yv195, yv196, yv197, bc) → new_foldl6(yv191, new_readInt0(yv191, yv192, yv193, bc), yv194, yv195, yv196, yv197, bc)
The graph contains the following edges 1 >= 1, 4 >= 3, 5 >= 4, 6 >= 5, 7 >= 6, 8 >= 7
- new_foldl1(yv145, yv146, yv147, yv148, yv151, ba) → new_foldl0(yv145, yv146, yv147, yv148, Succ(yv147), Succ(yv151), ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 6 >= 7
- new_foldl2(yv175, yv176, yv177, yv178, yv181, bb) → new_foldl4(yv175, yv176, new_pt(yv177, bb), yv178, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 4, 6 >= 5
- new_foldl0(yv175, yv176, yv177, yv178, Zero, Zero, bb) → new_foldl3(yv175, yv176, yv177, yv178, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 7 >= 5
- new_foldl(yv145, yv146, yv147, yv148, Zero, Zero, yv151, ba) → new_foldl1(yv145, yv146, yv147, yv148, yv151, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 7 >= 5, 8 >= 6
- new_foldl(yv145, yv146, yv147, yv148, Succ(yv1490), Zero, yv151, ba) → new_foldl0(yv145, yv146, yv147, yv148, Succ(yv147), Succ(yv151), ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 8 >= 7
- new_foldl0(yv175, yv176, yv177, yv178, Zero, Succ(yv1800), bb) → new_foldl2(yv175, yv176, yv177, yv178, new_span2Zs1(yv178), bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 7 >= 6
- new_foldl3(yv175, yv176, yv177, yv178, bb) → new_foldl2(yv175, yv176, yv177, yv178, new_span2Zs1(yv178), bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 6
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldr(yv59, yv60, yv61, Succ(yv620), Succ(yv630), ba) → new_foldr(yv59, yv60, yv61, yv620, yv630, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(yv59, yv60, yv61, Succ(yv620), Succ(yv630), ba) → new_foldr(yv59, yv60, yv61, yv620, yv630, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5, 6 >= 6
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr0(yv28, yv29, yv30, Succ(yv310), Succ(yv320), yv33, ba) → new_foldr0(yv28, yv29, yv30, yv310, yv320, yv33, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr0(yv28, yv29, yv30, Succ(yv310), Succ(yv320), yv33, ba) → new_foldr0(yv28, yv29, yv30, yv310, yv320, yv33, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 > 5, 6 >= 6, 7 >= 7